Skip to content

[Merged by Bors] - feat(NumberTheory/Divisors): divisors antidiagonal tsum#28690

Closed
CBirkbeck wants to merge 40 commits intoleanprover-community:masterfrom
CBirkbeck:divisorsAntidiagonal_tsum
Closed

[Merged by Bors] - feat(NumberTheory/Divisors): divisors antidiagonal tsum#28690
CBirkbeck wants to merge 40 commits intoleanprover-community:masterfrom
CBirkbeck:divisorsAntidiagonal_tsum

Conversation

@CBirkbeck
Copy link
Copy Markdown
Collaborator

@CBirkbeck CBirkbeck commented Aug 20, 2025 •
edited
Loading

@github-actions
Copy link
Copy Markdown

github-actions bot commented Aug 20, 2025 •
edited
Loading

PR summary 8bd4d3ea3d

Import changes exceeding 2%

% File
+119.28% Mathlib.NumberTheory.TsumDivsorsAntidiagonal

Import changes for modified files

Dependency changes

File Base Count Head Count Change
Mathlib.NumberTheory.TsumDivsorsAntidiagonal 726 1592 +866 (+119.28%)
Import changes for all files
Files Import difference
Mathlib.NumberTheory.TsumDivsorsAntidiagonal 866

Declarations diff

+ Summable.mul_tendsto_const
+ norm_natCast
+ sigma_eq_sum_div
+ summable_norm_pow_mul_geometric_div_one_sub
+ summable_prod_mul_pow
+ tprod_congr₂
+ tsum_pow_div_one_sub_eq_tsum_sigma
+ tsum_prod_pow_eq_tsum_sigma

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@CBirkbeck CBirkbeck mentioned this pull request Aug 20, 2025
Closed
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Aug 20, 2025
@CBirkbeck CBirkbeck mentioned this pull request Aug 20, 2025
Closed
9 tasks
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Aug 21, 2025
@mathlib4-dependent-issues-bot
Copy link
Copy Markdown
Collaborator

mathlib4-dependent-issues-bot commented Aug 21, 2025

This PR/issue depends on:

@github-actions github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Aug 21, 2025
@CBirkbeck CBirkbeck marked this pull request as ready for review August 21, 2025 09:10
CBirkbeck
CBirkbeck commented Sep 5, 2025
View reviewed changes
Comment thread Mathlib/Analysis/RCLike/Basic.lean
Comment thread Mathlib/Analysis/Normed/Group/Basic.lean
Comment thread Mathlib/Analysis/Complex/Norm.lean
Comment thread Mathlib/Analysis/Complex/Norm.lean
Comment thread Mathlib/Analysis/Complex/Exponential.lean
CBirkbeck and others added 4 commits September 5, 2025 14:27
@CBirkbeck
Copy link
Copy Markdown
Collaborator Author

CBirkbeck commented Sep 5, 2025 •
edited
Loading

I think I was talking rubbish earlier about the norm_natCast simp lemmas. I think you can just revert the changes in Mathlib/Analysis/Complex/Exponential.lean, Mathlib/Analysis/Complex/Norm.lean, Mathlib/Analysis/RCLike/Basic.lean and Mathlib/Analysis/Normed/Group/Basic.lean. I was mistaken in thinking this would somehow conflict with the general simp lemma you're adding in Mathlib/Analysis/Normed/Module/Basic.lean. (What I missed is that when the specific norm_natCast lemmas for ℝ, ℂ and an RCLike are stated, mathlib doesn't yet know that these types have an [NormSMulClass ℤ -] instance, because it is only created later using precisely these lemmas!)

So that was a complete distraction from the actual content of this PR. I hope to have some time to look at this properly either tomorrow, or early next week.

Hmm well the build was failing at the RCLike file, so that one does need changing. I think it does break at the other places as well, but I'll see if it builds first before changing them. Edit: Yep it breaks without this.

@loefflerd loefflerd mentioned this pull request Sep 5, 2025
Closed
@loefflerd
Copy link
Copy Markdown
Contributor

loefflerd commented Sep 5, 2025

Hmm well the build was failing at the RCLike file, so that one does need changing. I think it does break at the other places as well, but I'll see if it builds first before changing them. Edit: Yep it breaks without this.

I'm surprised. I made #29386, which is a fork of this PR, so I can play around with the simp-tagging changes. I will experiment & get back to you.

@loefflerd
Copy link
Copy Markdown
Contributor

loefflerd commented Sep 5, 2025

... and it genuinely doesn't work. Looks like I was actually correct first time around in guessing that the simp lemmas would need corrective action downstream. OK, I believe now that the current state of this PR is the Right Thing.

loefflerd
loefflerd reviewed Sep 8, 2025
View reviewed changes
Copy link
Copy Markdown
Contributor

@loefflerd loefflerd left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this is pretty much ready now. Some of the lemmas maybe don't look "natural" in their statements but this is probably inevitable for an early stage of a large multi-PR project.

maintainer delegate

Comment thread Mathlib/Analysis/Asymptotics/Lemmas.lean Outdated
Comment thread Mathlib/Analysis/Asymptotics/Lemmas.lean Outdated
Comment thread Mathlib/Analysis/Normed/Module/Basic.lean Outdated
Comment thread Mathlib/NumberTheory/TsumDivsorsAntidiagonal.lean Outdated
Comment thread Mathlib/NumberTheory/TsumDivsorsAntidiagonal.lean Outdated
Comment thread Mathlib/NumberTheory/TsumDivsorsAntidiagonal.lean Outdated
@github-actions
Copy link
Copy Markdown

github-actions bot commented Sep 8, 2025

🚀 Pull request has been placed on the maintainer queue by loefflerd.

@ghost ghost added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Sep 8, 2025
@riccardobrasca
Copy link
Copy Markdown
Member

riccardobrasca commented Sep 8, 2025

Thanks!

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Sep 8, 2025

✌️ CBirkbeck can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@ghost ghost added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Sep 8, 2025
@CBirkbeck
Copy link
Copy Markdown
Collaborator Author

CBirkbeck commented Sep 8, 2025

bors r+

mathlib-bors bot pushed a commit that referenced this pull request Sep 8, 2025
@CBirkbeck
feat(NumberTheory/Divisors): divisors antidiagonal tsum (#28690)
8e47256
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Sep 8, 2025

Build failed (retrying...):

mathlib-bors bot pushed a commit that referenced this pull request Sep 8, 2025
@CBirkbeck
feat(NumberTheory/Divisors): divisors antidiagonal tsum (#28690)
9d6c05b
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Sep 8, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(NumberTheory/Divisors): divisors antidiagonal tsum [Merged by Bors] - feat(NumberTheory/Divisors): divisors antidiagonal tsum Sep 8, 2025
@mathlib-bors mathlib-bors bot closed this Sep 8, 2025
yuanyi-350 pushed a commit to yuanyi-350/yuanyi_mathlib4 that referenced this pull request Sep 10, 2025
@CBirkbeck @yuanyi-350
feat(NumberTheory/Divisors): divisors antidiagonal tsum (leanprover-c…
f9a59ca 
…ommunity#28690)
robertmaxton42 pushed a commit to robertmaxton42/mathlib4 that referenced this pull request Sep 11, 2025
@CBirkbeck @robertmaxton42
feat(NumberTheory/Divisors): divisors antidiagonal tsum (leanprover-c…
611298f 
…ommunity#28690)
joelriou pushed a commit to joelriou/mathlib4 that referenced this pull request Oct 2, 2025
@CBirkbeck @joelriou
feat(NumberTheory/Divisors): divisors antidiagonal tsum (leanprover-c…
bbba257 
…ommunity#28690)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@loefflerd loefflerd loefflerd left review comments

Assignees

@jcommelin jcommelin

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). large-import Automatically added label for PRs with a significant increase in transitive imports t-number-theory Number theory (also use t-algebra or t-analysis to specialize)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@CBirkbeck @mathlib4-dependent-issues-bot @loefflerd @riccardobrasca @jcommelin
⚡